A class of confluent term rewriting systems and unification
Identifieur interne : 00E861 ( Main/Exploration ); précédent : 00E860; suivant : 00E862A class of confluent term rewriting systems and unification
Auteurs : Jia-Huai You [Canada] ; P. A. Subrahmanyam [États-Unis]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 1986-12-01.
English descriptors
- KwdEn :
- Teeft :
- Algorithm, Canonical, Canonical term, Closure, Closure property, Complete algorithm, Complete sets, Complete unification algorithm, Completeness proof, Computer science, Confluence, Confluence property, Confluent, Confluent term, Equational, Equational programs, Equational theories, Equational theory, Equivalence classes, First occurrence, Function symbol, Functional programs, Input terms, Lefthand, Lefthand side, Linear term, Logic programming, Major transformation step, Minimum unifier, Normal form, Other hand, Proc, Reducible subterm, Reduction sequence, Reduction sequences, Residue, Righthand side, Second clause, Subrahmanyam, Substitution, Subterm, Subterms, Such equivalence classes, Theorem prover, Transformation process, Unification, Unifier.
Abstract
Abstract: The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.
Url:
DOI: 10.1007/BF00248250
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001842
- to stream Istex, to step Curation: 001823
- to stream Istex, to step Checkpoint: 003647
- to stream Main, to step Merge: 00F149
- to stream Main, to step Curation: 00E861
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A class of confluent term rewriting systems and unification</title><author><name sortKey="You, Jia Huai" sort="You, Jia Huai" uniqKey="You J" first="Jia-Huai" last="You">Jia-Huai You</name></author><author><name sortKey="Subrahmanyam, P A" sort="Subrahmanyam, P A" uniqKey="Subrahmanyam P" first="P. A." last="Subrahmanyam">P. A. Subrahmanyam</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:68E6ED1447766E95E1441638585383807D736062</idno><date when="1986" year="1986">1986</date><idno type="doi">10.1007/BF00248250</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-X2CQM9FX-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001842</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001842</idno><idno type="wicri:Area/Istex/Curation">001823</idno><idno type="wicri:Area/Istex/Checkpoint">003647</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003647</idno><idno type="wicri:doubleKey">0168-7433:1986:You J:a:class:of</idno><idno type="wicri:Area/Main/Merge">00F149</idno><idno type="wicri:Area/Main/Curation">00E861</idno><idno type="wicri:Area/Main/Exploration">00E861</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A class of confluent term rewriting systems and unification</title><author><name sortKey="You, Jia Huai" sort="You, Jia Huai" uniqKey="You J" first="Jia-Huai" last="You">Jia-Huai You</name><affiliation wicri:level="1"><country xml:lang="fr">Canada</country><wicri:regionArea>Department of Computing Science, University of Alberta, T6G 2H1, Edmonton, Alberta</wicri:regionArea><wicri:noRegion>Alberta</wicri:noRegion></affiliation></author><author><name sortKey="Subrahmanyam, P A" sort="Subrahmanyam, P A" uniqKey="Subrahmanyam P" first="P. A." last="Subrahmanyam">P. A. Subrahmanyam</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>AT&T Bell Laboratories, 07733, Holmdel, NJ</wicri:regionArea><placeName><region type="state">New Jersey</region></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="1986-12-01">1986-12-01</date><biblScope unit="volume">2</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="391">391</biblScope><biblScope unit="page" to="418">418</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>E-unification</term><term>Term rewriting systems</term><term>equational theories</term><term>narrowing</term></keywords><keywords scheme="Teeft" xml:lang="en"><term>Algorithm</term><term>Canonical</term><term>Canonical term</term><term>Closure</term><term>Closure property</term><term>Complete algorithm</term><term>Complete sets</term><term>Complete unification algorithm</term><term>Completeness proof</term><term>Computer science</term><term>Confluence</term><term>Confluence property</term><term>Confluent</term><term>Confluent term</term><term>Equational</term><term>Equational programs</term><term>Equational theories</term><term>Equational theory</term><term>Equivalence classes</term><term>First occurrence</term><term>Function symbol</term><term>Functional programs</term><term>Input terms</term><term>Lefthand</term><term>Lefthand side</term><term>Linear term</term><term>Logic programming</term><term>Major transformation step</term><term>Minimum unifier</term><term>Normal form</term><term>Other hand</term><term>Proc</term><term>Reducible subterm</term><term>Reduction sequence</term><term>Reduction sequences</term><term>Residue</term><term>Righthand side</term><term>Second clause</term><term>Subrahmanyam</term><term>Substitution</term><term>Subterm</term><term>Subterms</term><term>Such equivalence classes</term><term>Theorem prover</term><term>Transformation process</term><term>Unification</term><term>Unifier</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.</div></front></TEI><affiliations><list><country><li>Canada</li><li>États-Unis</li></country><region><li>New Jersey</li></region></list><tree><country name="Canada"><noRegion><name sortKey="You, Jia Huai" sort="You, Jia Huai" uniqKey="You J" first="Jia-Huai" last="You">Jia-Huai You</name></noRegion></country><country name="États-Unis"><region name="New Jersey"><name sortKey="Subrahmanyam, P A" sort="Subrahmanyam, P A" uniqKey="Subrahmanyam P" first="P. A." last="Subrahmanyam">P. A. Subrahmanyam</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00E861 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00E861 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:68E6ED1447766E95E1441638585383807D736062
|texte= A class of confluent term rewriting systems and unification
}}
| This area was generated with Dilib version V0.6.33. |  |